A, B:Type, L:((A(B + Top)) List), x:A.
(can-apply(p-first(L);x))
 (do-apply(p-first(L);x) = do-apply(hd(filter(f.can-apply(f;x);L));x)  B) 

latex

Definitions	Top, t  T, left + right, x:AB(x), type List, b, s = t, P  Q, x:A. B(x), Type, False, p_first_nil{p_first_nil_compseq_tag_def:ObjectId}(x), hd(l), [], [car / cdr], as @ bs, s ~ t, P  Q, Dec(P), x:A  B(x), P & Q, P  Q, True, T, , , P  Q, p-first(L), can-apply(f;x), A, b, Void, x:A.B(x), S  T, suptype(S; T), Unit, do-apply(f;x), f(a), x.A(x), {T}, SQType(T), outl(x), [f?g]
Lemmas	outl wf, do-apply wf, append wf, true wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, p-first-append, assert wf, p-conditional-to-p-first, p-conditional-domain, decidable assert, can-apply wf, p-first wf, false wf, top wf